#include <iostream>
#include <fstream>
#include <sstream>
#include <vector>
#include <set>


using namespace std;

typedef vector<int> VI;
typedef vector<vector<int> > VVI;

void read3cnf(VVI& F, VVI& S, int& num_lit, char *filename) {
    ifstream infile;
    infile.open(filename);
    string s;
    bool eof = false;
    if (infile.is_open()) {
        while (infile.good() and not eof) {
            getline (infile, s);
            if (not (s[0] == 'c')) {
                stringstream sts(s);
                if (s[0] == 'p') {
                    char dummychar;
                    string dummystring;
                    sts >> dummychar >> dummystring >> num_lit;
                } 
                else if (s[0] == '%') eof = true;
                else {
                    int l1, l2, l3;
                    sts >> l1 >> l2 >> l3;
                    
                    VI f(3);
                    VI s(3);
                    f[0] = abs(l1);
                    s[0] = sign(l1);
                    f[1] = abs(l2);
                    s[1] = sign(l2);
                    f[2] = abs(l3);
                    s[2] = sign(l3);
                    
                    F.push_back(f); 
                    S.push_back(s);
                }
            }
        }
        infile.close();
        //cout << "nump = " << num_lit << endl;
        /*for (int i = 0; i < P.size(); ++i) {
            for (int j = 0; j < P[0].size(); j += 3) {
                cout << P[i][j] << "," << P[i][j+1] << "," << P[i][j+2] << endl;
            }
        }*/
    } 
    else cout << "Unable to open file" << endl;
}


bool check_consistency(const VI& model, const VVI& F, const VVI& S, const VVI& lit_a, const LI& ch_list) {
    for (LIIt it = ch_list.begin(); it != ch_list.end(); ++it) {
        for (int i = 0; i < lit_a[*it].size(); ++i) {
            int cl = lit_a[*it][i];
            if (info[cl]) {
                int s = 0;
                int claus_size = F[cl].size();
                for (int j = 0; s > 0 and j < claus_size; ++j) {
                    int val = model[F[cl][j]];
                    if (val == -1) {
                        ++s;
                    }
                    else s += abs(val - S[cl][j]);
                }
                if (s == 0) return false;
            }
        }
    }
    return true;
}
	
void choose_lit(const VVI& F, const VVI& lit_a, const VB& info, const VI& model, const VI& pos, const VI& neg, int& l, int& i) {
    int max = -1;
    for (int i = 0; i < lit_a.size(); ++i) {
        if (model[i] == -1) {
            for (int j = 0; j < lit_a[i].size(); ++j) {
                int s = 0;
                if (info[lit_a[i][j]]) ++s;
            }
            if (s > max) {
                max = s;
                l = i;
            }
        }
    }
    i = (pos[l] < neg[l]) ? 1 : 0;
}

void propagate(VI& model, const VVI& F, const VVI& lit_a, LI& ch_model, VI& info, LI& ch_info, int l) {
    for (int i = 0; i < lit_a[l].size(); ++i) {
        if (info[lit_a[l][i]]) {
               
        }
    }
}

void propagate(VI& model, const VVI& F, queue<int>& MQ , VI& claus, queue<int>& CQ, int l) {
	for (int i = 0; i < lit_a[l].size(); ++i) {
		if (sign[l] - model[l] == 1) {
			claus[i] = 1;
			CQ.push(i);
		} 
		if (claus[i] == 0) {
			int z = 0;
			int n = 0;
			int pos_n = 0;
			for (int j = 0; j < F[i].size(); ++j) {
				int eval = get_sign(F[i][j]) - model[abs(F[i][j])];
				if (eval == 0) ++z;
				else (eval == -1) {
					++n;
					pos_n = j;
				}
			}
			if (z == 2 and n == 1) {
				model[abs(F[i][j])] = 1 - get_sign(F[i][j]);
				MQ.push(F[i][j]);
				propagate(model, F, MQ, claus, CQ, F[i][j]);
			}
		}	
	} 
}

void dpll(VI& model, const VVI& F, const VVI& lit_a, VI& claus) {
	check_consistency(model, F, lit_a);
	if (model[0] == 1) {
		int l, i;
		choose_lit(F, claus, l, i);
		
		queue<int> MQ;
		model[l] = i;
		MQ.push(l);
		queue<int> CQ;
		propagate(model, F, MQ, claus, CQ, l);
		dpll(model, F, lit_a, claus);
		if (model[0] == 0) {
			while (!MQ.empty()) {
				model[MQ.front()] = -1;
				MQ.pop();
			}
			while (!CQ.empty()) {
				lit_a[MQ.front()] = 0;
			}
			model[l] = 1 - i;
	
			n = propagate(model, F, lit_c_b, lit_a, claus_b);
			dpll(model, F, lit_c_b, lit_a, claus_b);
		}
	}	
}

int main(int argc, char *argv[]) {
	
	// llegir formula F
	VVI F;
	int num_lit;
	read3cnf(F, num_lit, argv[1]);
	
	// contem aparicions positives i negatives de cada literal i a quines 
	// clausules apareix
	VVI lit_a(num_lit + 1);
	VVI lit_c(num_lit + 1, vector<int>(2, 0));
	for (int i = 0; i < F.size(); ++i) {
		for (int j = 0; j < F[i].size(); ++j) {
			++lit_c[abs(F[i][j])][get_sign(F[i][j])];
			lit_a[abs(F[i][j])].push_back(i);
		}

	//apliquem el dpll
	VI claus(F.size(), 0);
	VI model(num_lit + 1, -1);
	model[0] = 1;
	dpll(model, F, lit_c, lit_a, claus);

	//mostrar resultat [sat | unsat] i si es sat un model
	if (model[0] == 2) {
		cout << "SAT" << endl;
		for (int i = 1; i < model.size(); ++i) cout << model[i];
		cout << endl;
	}
	else cout << "UNSAT" << endl;
	
}
